Nuprl Lemma : ma-has-effect_wf
0,22
postcript
pdf
A
:MsgA,
k
:Knd. ma-has-effect(
A
;
k
)
Prop
latex
Definitions
Knd
,
t
T
,
Id
,
x
:
A
.
B
(
x
)
,
x
.
t
(
x
)
,
1of(
t
)
,
map(
f
;
as
)
,
KindDeq
,
deq-member(
eq
;
x
;
L
)
,
b
,
Prop
,
a
:
A
fp
B
(
a
)
,
ma-has-effect(
M
;
k
)
,
MsgA
Lemmas
msga
wf
,
assert
wf
,
deq-member
wf
,
Kind-deq
wf
,
map
wf
,
pi1
wf
,
Id
wf
,
Knd
wf
origin